--Expected Output: BufferOverflow

DEF MAIN:nat == mul(9223372036854775806,2)
